$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $L$:($T$ List), $i$:int\_seg(0; $\parallel$$L$$\parallel$).
\\[0ex]no\_repeats($T$; $L$) $\Rightarrow$ (mu(($\lambda$${\it i@}_{0}$.eqof(${\it eq}$)($L$[$i$],$L$[${\it i@}_{0}$]))) = $i$ $\in$ $\mathbb{Z}$)